harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_one_iff_eq_one_of_mul_eq_one {a b : M} (h : a * b = 1) : a = 1 ↔ b = 1

Proof state:
case mpr
M : Type u_4
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1

Tactic:
simpa using h

Result:
no goals

Proof state:
case mpr
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1

Tactic:
rintro rfl

Result:
case mpr
M : Type u_4
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1

Proof state:
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 ↔ b = 1

Tactic:
constructor <;> (rintro rfl; simpa using h)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem restrict_nonzero_iff (μ : FiniteMeasure Ω) (A : Set Ω) : μ.restrict A ≠ 0 ↔ μ A ≠ 0

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ μ.restrict A ≠ 0 ↔ μ A ≠ 0

Tactic:
rw [← mass_nonzero_iff, restrict_mass]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment)
      (input : BinaryRefVec aig w)
      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs.getLsbD idx)
      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs.getLsbD idx) :
      ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
          =
        (lhs * rhs).getLsbD idx

Proof state:
case isTrue
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
h✝ : RefVec.countKnown aig input.lhs < RefVec.countKnown aig input.rhs
hb : blastMul.blast aig input = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx

Tactic:
rw [← hb, blastMul.denote_blast] <;> assumption

Result:
no goals

Proof state:
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign.toAIGAssignment, { aig := (blastMul aig input).aig, ref := (blastMul aig input).vec.get idx hidx }⟧ =
    (lhs * rhs).getLsbD idx

Tactic:
generalize hb : blastMul aig input = res

Result:
w : Nat
aig : AIG BVBit
lhs rhs : BitVec w
assign : Assignment
input : aig.BinaryRefVec w
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry BVBit w
hb : blastMul aig input = res
⊢ ⟦assign.toAIGAssignment, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs * rhs).getLsbD idx
-- Mathlib/Analysis/Calculus/Deriv/Star.lean
theorem HasDerivAtFilter.star (h : HasDerivAtFilter f f' x L) :
    HasDerivAtFilter (fun x => star (f x)) (star f') x L

Proof state:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
inst✝⁴ : StarRing 𝕜
inst✝³ : TrivialStar 𝕜
inst✝² : StarAddMonoid F
inst✝¹ : ContinuousStar F
inst✝ : StarModule 𝕜 F
f' : F
x : 𝕜
L : Filter 𝕜
h : HasDerivAtFilter f f' x L
⊢ HasDerivAtFilter (fun x => star (f x)) (star f') x L

Tactic:
simpa using h.star.hasDerivAtFilter

Result:
no goals
-- Mathlib/Data/List/Iterate.lean
theorem iterate_add (f : α → α) (a : α) (m n : ℕ) :
    iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n

Proof state:
case zero
α : Type u_1
f : α → α
n : ℕ
a : α
⊢ iterate f a (0 + n) = iterate f a 0 ++ iterate f (f^[0] a) n

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
f : α → α
n✝ n : ℕ
ih : ∀ (a : α), iterate f a (n + n✝) = iterate f a n ++ iterate f (f^[n] a) n✝
a : α
⊢ iterate f a (n + 1 + n✝) = iterate f a (n + 1) ++ iterate f (f^[n + 1] a) n✝

Tactic:
rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
a : α
m n : ℕ
⊢ iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n

Tactic:
induction m generalizing a with
| zero => simp
| succ n ih => rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_inf_mul_relrank_of_le (h : A ≤ B) :
    A.relrank (B ⊓ C) * B.relrank C = A.relrank C

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : A ≤ B
⊢ A.relrank (B ⊓ C) * B.relrank C = A.relrank C

Tactic:
simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.isCircuit_restrict_of_subset (hC : M.IsCircuit C) (hCR : C ⊆ R) :
    (M ↾ R).IsCircuit C

Proof state:
α : Type u_1
M : Matroid α
C R : Set α
hC : M.IsCircuit C
hCR : C ⊆ R
⊢ (M ↾ R).IsCircuit C

Tactic:
simp_rw [isCircuit_iff, restrict_dep_iff, dep_iff, and_imp] at *

Result:
α : Type u_1
M : Matroid α
C R : Set α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ M.E → D ⊆ C → D = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C

Proof state:
α : Type u_1
M : Matroid α
C R : Set α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ M.E → D ⊆ C → D = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C

Tactic:
exact ⟨⟨hC.1.1, hCR⟩, fun I hI _ hIC ↦ hC.2 hI (hIC.trans hC.1.2) hIC⟩

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem shiftRight_add' : ∀ (m : ℤ) (n k : ℕ), m >>> (n + k : ℤ) = (m >>> (n : ℤ)) >>> (k : ℤ)
  | (m : ℕ), n, k => by
    rw [shiftRight_coe_nat, shiftRight_coe_nat, ← Int.ofNat_add, shiftRight_coe_nat,
      Nat.shiftRight_add]
  | -[m+1], n, k => by
    rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.ofNat_add, shiftRight_negSucc,
      Nat.shiftRight_add]

Proof state:
m n k : ℕ
⊢ -[m+1] >>> (↑n + ↑k) = -[m+1] >>> ↑n >>> ↑k

Tactic:
rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.ofNat_add, shiftRight_negSucc,
  Nat.shiftRight_add]

Result:
no goals

Proof state:
m n k : ℕ
⊢ ↑m >>> (↑n + ↑k) = ↑m >>> ↑n >>> ↑k

Tactic:
rw [shiftRight_coe_nat, shiftRight_coe_nat, ← Int.ofNat_add, shiftRight_coe_nat,
  Nat.shiftRight_add]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Ultra.lean
lemma isUltrametricDist_of_forall_norm_sub_one_of_norm_le_one
    (h : ∀ x : R, ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1) : IsUltrametricDist R

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
this : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
⊢ IsUltrametricDist R

Tactic:
exact isUltrametricDist_of_forall_norm_add_one_of_norm_le_one this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
x : R
hx : ‖x‖ ≤ 1
⊢ ‖x + 1‖ ≤ 1

Tactic:
simpa only [← neg_add', norm_neg] using h (-x) (norm_neg x ▸ hx)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
⊢ IsUltrametricDist R

Tactic:
have (x : R) (hx : ‖x‖ ≤ 1) : ‖x + 1‖ ≤ 1 := by
  simpa only [← neg_add', norm_neg] using h (-x) (norm_neg x ▸ hx)

Result:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
this : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
⊢ IsUltrametricDist R
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_const_const_iff [NeBot l] {d : E''} {c : F''} :
    ((fun _x => d) =o[l] fun _x => c) ↔ d = 0

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
⊢ ((fun _x => d) =o[l] fun _x => c) ↔ d = 0

Tactic:
simp only [isLittleO_const_left, or_iff_left_iff_imp]

Result:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
⊢ Tendsto (norm ∘ fun _x => c) l atTop → d = 0

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
⊢ Tendsto (norm ∘ fun _x => c) l atTop → d = 0

Tactic:
exact fun h => (this h).elim

Result:
no goals

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
d : E''
c : F''
⊢ ((fun _x => d) =o[l] fun _x => c) ↔ d = 0

Tactic:
have : ¬Tendsto (Function.const α ‖c‖) l atTop :=
  not_tendsto_atTop_of_tendsto_nhds tendsto_const_nhds

Result:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
⊢ ((fun _x => d) =o[l] fun _x => c) ↔ d = 0
-- Mathlib/Topology/ContinuousMap/Interval.lean
theorem IccExtendCM_of_mem {f : C(Icc a b, E)} {x : α} (hx : x ∈ Icc a b) :
    IccExtendCM f x = f ⟨x, hx⟩

Proof state:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a b : α
inst✝¹ : Fact (a ≤ b)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
x : α
hx : x ∈ Icc a b
⊢ (IccExtendCM f) x = f ⟨x, hx⟩

Tactic:
simp [IccExtendCM, projIccCM, projIcc, hx.1, hx.2]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem Integrable.smul {c : 𝕜} {f : α →ₘ[μ] β} : Integrable f → Integrable (c • f) :=
  induction_on f fun _f hfm hfi => (integrable_mk _).2 <|
    by simpa using ((integrable_mk hfm).1 hfi).smul c

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α →ₘ[μ] β
_f : α → β
hfm : AEStronglyMeasurable _f μ
hfi : (mk _f hfm).Integrable
⊢ MeasureTheory.Integrable ((fun x => c • x) ∘ ↑⟨_f, hfm⟩) μ

Tactic:
simpa using ((integrable_mk hfm).1 hfi).smul c

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem trans {q' : Set α → Prop} (H : InnerRegularWRT μ p q) (H' : InnerRegularWRT μ q q') :
    InnerRegularWRT μ p q'

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
⊢ ∃ K ⊆ U, p K ∧ r < μ K

Tactic:
rcases H' hU r hr with ⟨F, hFU, hqF, hF⟩

Result:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < μ F
⊢ ∃ K ⊆ U, p K ∧ r < μ K

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
⊢ μ.InnerRegularWRT p q'

Tactic:
intro U hU r hr

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
⊢ ∃ K ⊆ U, p K ∧ r < μ K

Proof state:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < μ F
⊢ ∃ K ⊆ U, p K ∧ r < μ K

Tactic:
rcases H hqF _ hF with ⟨K, hKF, hpK, hrK⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < μ F
K : Set α
hKF : K ⊆ F
hpK : p K
hrK : r < μ K
⊢ ∃ K ⊆ U, p K ∧ r < μ K

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < μ F
K : Set α
hKF : K ⊆ F
hpK : p K
hrK : r < μ K
⊢ ∃ K ⊆ U, p K ∧ r < μ K

Tactic:
exact ⟨K, hKF.trans hFU, hpK, hrK⟩

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
lemma isOpen_symm_image_iff_of_subset_target {t : Set Y} (hs : t ⊆ e.target) :
    IsOpen (e.symm '' t) ↔ IsOpen t

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen (↑e.symm '' t)
hs' : ↑e.symm '' t ⊆ e.source
⊢ IsOpen t

Tactic:
rw [← e.image_symm_image_of_subset_target hs]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen (↑e.symm '' t)
hs' : ↑e.symm '' t ⊆ e.source
⊢ IsOpen (↑e.toPartialEquiv '' (↑e.symm '' t))

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen (↑e.symm '' t)
⊢ IsOpen t

Tactic:
have hs' : e.symm '' t ⊆ e.source := by
  rw [e.symm_image_eq_source_inter_preimage hs]
  apply Set.inter_subset_left

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen (↑e.symm '' t)
hs' : ↑e.symm '' t ⊆ e.source
⊢ IsOpen t

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen (↑e.symm '' t)
hs' : ↑e.symm '' t ⊆ e.source
⊢ IsOpen (↑e.toPartialEquiv '' (↑e.symm '' t))

Tactic:
exact e.isOpen_image_of_subset_source h hs'

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
⊢ IsOpen (↑e.symm '' t) ↔ IsOpen t

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ e.symm.isOpen_image_of_subset_source h hs⟩

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen (↑e.symm '' t)
⊢ IsOpen t

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen (↑e.symm '' t)
⊢ e.source ∩ ↑e ⁻¹' t ⊆ e.source

Tactic:
apply Set.inter_subset_left

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen (↑e.symm '' t)
⊢ ↑e.symm '' t ⊆ e.source

Tactic:
rw [e.symm_image_eq_source_inter_preimage hs]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen (↑e.symm '' t)
⊢ e.source ∩ ↑e ⁻¹' t ⊆ e.source
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.eqToHom_comp_ι (f : J → C) [HasBiproduct f] {j j' : J} (w : j = j') :
    eqToHom (by simp [w]) ≫ biproduct.ι f j' = biproduct.ι f j

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j j' : J
w : j = j'
⊢ eqToHom ⋯ ≫ ι f j' = ι f j

Tactic:
cases w

Result:
case refl
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ eqToHom ⋯ ≫ ι f j = ι f j

Proof state:
case refl
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ eqToHom ⋯ ≫ ι f j = ι f j

Tactic:
simp

Result:
no goals

Proof state:
J✝ : Type w
C✝ : Type uC
inst✝⁶ : Category.{uC', uC} C✝
inst✝⁵ : HasZeroMorphisms C✝
D : Type uD
inst✝⁴ : Category.{uD', uD} D
inst✝³ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
@[simp]
lemma map_toMatrix [DecidableEq n] [NonAssocSemiring α] [NonAssocSemiring β]
    (f : α →+* β) (σ : m ≃. n) : σ.toMatrix.map f = σ.toMatrix

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : NonAssocSemiring β
f : α →+* β
σ : m ≃. n
⊢ σ.toMatrix.map ⇑f = σ.toMatrix

Tactic:
ext i j

Result:
case a
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : NonAssocSemiring β
f : α →+* β
σ : m ≃. n
i : m
j : n
⊢ σ.toMatrix.map (⇑f) i j = σ.toMatrix i j

Proof state:
case a
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : NonAssocSemiring β
f : α →+* β
σ : m ≃. n
i : m
j : n
⊢ σ.toMatrix.map (⇑f) i j = σ.toMatrix i j

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean
theorem ContMDiffAt.prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀) :
    ContMDiffAt I' I n (fun x ↦ ∏ i ∈ t, f i x) x₀

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀
⊢ ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x₀

Tactic:
simp only [← contMDiffWithinAt_univ] at *

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) Set.univ x₀
⊢ ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) Set.univ x₀

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) Set.univ x₀
⊢ ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) Set.univ x₀

Tactic:
exact ContMDiffWithinAt.prod h

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_equation (hf : Function.Injective f) (P : Fin 3 → A) :
    (W'.baseChange B).toJacobian.Equation (f ∘ P) ↔ (W'.baseChange A).toJacobian.Equation P

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (baseChange W' B).toJacobian.Equation (⇑f ∘ P) ↔ (baseChange W' A).toJacobian.Equation P

Tactic:
rw [← RingHom.coe_coe, ← map_equation hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma mapEquiv_isBasis_iff {α β : Type*} {M : Matroid α} (f : α ≃ β) {I X : Set β} :
    (M.mapEquiv f).IsBasis I X ↔ M.IsBasis (f.symm '' I) (f.symm '' X)

Proof state:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)
⊢ I = ⇑f '' (⇑f.symm '' I)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
⊢ (M.mapEquiv f).IsBasis I X ↔ M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)

Tactic:
rw [mapEquiv_eq_map, map_isBasis_iff']

Result:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) ↔ M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)

Proof state:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀
⊢ M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)

Tactic:
obtain ⟨I, X, hIX, rfl, rfl⟩ := h

Result:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set α
hIX : M.IsBasis I X
⊢ M.IsBasis (⇑f.symm '' (⇑f '' I)) (⇑f.symm '' (⇑f '' X))

Proof state:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)
⊢ X = ⇑f '' (⇑f.symm '' X)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) ↔ M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨_, _, h, by simp, by simp⟩⟩

Result:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀
⊢ M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)

Proof state:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set α
hIX : M.IsBasis I X
⊢ M.IsBasis (⇑f.symm '' (⇑f '' I)) (⇑f.symm '' (⇑f '' X))

Tactic:
simpa

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_iff (P : Fin 3 → R) : W'.Nonsingular P ↔ W'.Equation P ∧
    (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) ≠ 0 ∨
      2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 ≠ 0 ∨
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z
        - (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) ≠ 0)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.Nonsingular P ↔
    W'.Equation P ∧
      (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) ≠ 0 ∨
        2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 ≠ 0 ∨
          P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
              (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) ≠
            0)

Tactic:
rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]

Result:
no goals