harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
lemma congr_apply {X} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} (x : Meq P S) {Y}
    {f g : Y ⟶ X} (h : f = g) (hf : S f) :
    x ⟨_, _, hf⟩ = x ⟨_, g, by simpa only [← h] using hf⟩

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
Y : C
f g : Y ⟶ X
h : f = g
hf : (↑S).arrows f
⊢ ↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := g, hf := ⋯ }

Tactic:
subst h

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
Y : C
f : Y ⟶ X
hf : (↑S).arrows f
⊢ ↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := f, hf := ⋯ }

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
Y : C
f : Y ⟶ X
hf : (↑S).arrows f
⊢ ↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := f, hf := ⋯ }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
Y : C
f g : Y ⟶ X
h : f = g
hf : (↑S).arrows f
⊢ (↑S).arrows g

Tactic:
simpa only [← h] using hf

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem surjective_of_injective {f : α → α} (hinj : Injective f) : Surjective f

Proof state:
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
⊢ ∃ a, f a = x

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
⊢ ∃ a, f a = x

Proof state:
case intro.intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
y : α
h : y ∈ univ ∧ f y = x
⊢ ∃ a, f a = x

Tactic:
exact ⟨y, h.2⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
⊢ ∃ a, f a = x

Tactic:
obtain ⟨y, h⟩ := mem_image.1 h₂

Result:
case intro.intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
y : α
h : y ∈ univ ∧ f y = x
⊢ ∃ a, f a = x

Proof state:
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
⊢ ∃ a, f a = x

Tactic:
have := Classical.propDecidable

Result:
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
⊢ ∃ a, f a = x

Proof state:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
⊢ ∃ a, f a = x

Tactic:
have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x

Result:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
⊢ ∃ a, f a = x

Proof state:
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
⊢ Surjective f

Tactic:
intro x

Result:
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
⊢ ∃ a, f a = x

Proof state:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
⊢ ∃ a, f a = x

Tactic:
have h₁ : image f univ = univ :=
  eq_of_subset_of_card_le (subset_univ _)
    ((card_image_of_injective univ hinj).symm ▸ le_rfl)

Result:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
⊢ ∃ a, f a = x
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Associates.le_singleton_iff (x : A) (n : ℕ) (I : Ideal A) :
    Associates.mk I ^ n ≤ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
x : A
n : ℕ
I : Ideal A
⊢ Associates.mk I ^ n ≤ Associates.mk (span {x}) ↔ x ∈ I ^ n

Tactic:
simp_rw [← Associates.dvd_eq_le, ← Associates.mk_pow, Associates.mk_dvd_mk,
  Ideal.dvd_span_singleton]

Result:
no goals
-- Mathlib/Topology/Instances/Real/Lemmas.lean
theorem Real.subfield_eq_of_closed {K : Subfield ℝ} (hc : IsClosed (K : Set ℝ)) : K = ⊤

Proof state:
K : Subfield ℝ
hc : IsClosed ↑K
⊢ range Rat.cast ⊆ ↑K

Tactic:
rintro - ⟨_, rfl⟩

Result:
case intro
K : Subfield ℝ
hc : IsClosed ↑K
w✝ : ℚ
⊢ ↑w✝ ∈ ↑K

Proof state:
case intro
K : Subfield ℝ
hc : IsClosed ↑K
w✝ : ℚ
⊢ ↑w✝ ∈ ↑K

Tactic:
exact SubfieldClass.ratCast_mem K _

Result:
no goals

Proof state:
K : Subfield ℝ
hc : IsClosed ↑K
⊢ K = ⊤

Tactic:
rw [SetLike.ext'_iff, Subfield.coe_top, ← hc.closure_eq]

Result:
K : Subfield ℝ
hc : IsClosed ↑K
⊢ closure ↑K = univ

Proof state:
K : Subfield ℝ
hc : IsClosed ↑K
⊢ closure ↑K = univ

Tactic:
refine Rat.denseRange_cast.mono ?_ |>.closure_eq

Result:
K : Subfield ℝ
hc : IsClosed ↑K
⊢ range Rat.cast ⊆ ↑K
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma MemHolder.nnHolderNorm_smul {α} [NormedDivisionRing α] [Module α Y] [BoundedSMul α Y]
    (hf : MemHolder r f) (c : α) :
    nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
hf : MemHolder r f
c : α
⊢ nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f

Tactic:
rw [← ENNReal.coe_inj, coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm,
  hf.smul.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_smul]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
lemma homologyι_truncGE'XIsoOpcycles_inv_d :
    (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

Tactic:
by_cases hjk : c.Rel j k

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : ¬c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : ¬c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

Tactic:
rw [shape _ _ _ hjk, comp_zero]

Result:
no goals

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

Tactic:
rw [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj, assoc, Iso.inv_hom_id_assoc,
homologyι_comp_fromOpcycles_assoc, zero_comp]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_triangle (a b c : α) : a \ c ≤ a \ b ⊔ b \ c

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ c ≤ a \ b ⊔ b \ c

Tactic:
rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ (a \ b) ≤ c ⊔ b \ c

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ (a \ b) ≤ c ⊔ b \ c

Tactic:
exact sdiff_sdiff_le.trans le_sup_sdiff

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_six [CommMonoid β] (f : Fin 6 → β) :
    ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 6 → β
⊢ ∏ i : Fin 6, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5

Tactic:
rw [prod_univ_castSucc, prod_univ_five]

Result:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 6 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (last 5) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 6 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (last 5) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.aestronglyMeasurable_add_measure_iff [PseudoMetrizableSpace β] {ν : Measure α} :
    AEStronglyMeasurable f (μ + ν) ↔ AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (bif true then μ else ν) ∧ AEStronglyMeasurable f (bif false then μ else ν) ↔
    AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (μ + ν) ↔ AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν

Tactic:
rw [← sum_cond, aestronglyMeasurable_sum_measure_iff, Bool.forall_bool, and_comm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (bif true then μ else ν) ∧ AEStronglyMeasurable f (bif false then μ else ν) ↔
    AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHom_homOf_eq_self (z : Cocycle F G 0) : ofHom (homOf z) = z

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cocycle F G 0
⊢ ofHom z.homOf = z

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem exists_cons_eq_concat {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
    ∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w), cons h p = q.concat h'

Proof state:
case cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q, ∃ (h' : G.Adj x w✝), cons h p = q.concat h'
u : V
h : G.Adj u u✝
⊢ ∃ x q, ∃ (h'_1 : G.Adj x w✝), cons h (cons h' p) = q.concat h'_1

Tactic:
obtain ⟨y, q, h'', hc⟩ := ih h'

Result:
case cons.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q, ∃ (h' : G.Adj x w✝), cons h p = q.concat h'
u : V
h : G.Adj u u✝
y : V
q : G.Walk u✝ y
h'' : G.Adj y w✝
hc : cons h' p = q.concat h''
⊢ ∃ x q, ∃ (h'_1 : G.Adj x w✝), cons h (cons h' p) = q.concat h'_1

Proof state:
case cons.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q, ∃ (h' : G.Adj x w✝), cons h p = q.concat h'
u : V
h : G.Adj u u✝
y : V
q : G.Walk u✝ y
h'' : G.Adj y w✝
hc : cons h' p = q.concat h''
⊢ ∃ x q, ∃ (h'_1 : G.Adj x w✝), cons h (cons h' p) = q.concat h'_1

Tactic:
refine ⟨y, cons h q, h'', ?_⟩

Result:
case cons.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q, ∃ (h' : G.Adj x w✝), cons h p = q.concat h'
u : V
h : G.Adj u u✝
y : V
q : G.Walk u✝ y
h'' : G.Adj y w✝
hc : cons h' p = q.concat h''
⊢ cons h (cons h' p) = (cons h q).concat h''

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ ∃ x q, ∃ (h' : G.Adj x w), cons h p = q.concat h'

Tactic:
induction p generalizing u with
| nil => exact ⟨_, nil, h, rfl⟩
| cons h' p ih =>
  obtain ⟨y, q, h'', hc⟩ := ih h'
  refine ⟨y, cons h q, h'', ?_⟩
  rw [concat_cons, hc]

Result:
no goals

Proof state:
case cons.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q, ∃ (h' : G.Adj x w✝), cons h p = q.concat h'
u : V
h : G.Adj u u✝
y : V
q : G.Walk u✝ y
h'' : G.Adj y w✝
hc : cons h' p = q.concat h''
⊢ cons h (cons h' p) = (cons h q).concat h''

Tactic:
rw [concat_cons, hc]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
v w u✝ u : V
h : G.Adj u u✝
⊢ ∃ x q, ∃ (h' : G.Adj x u✝), cons h nil = q.concat h'

Tactic:
exact ⟨_, nil, h, rfl⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_polynomialY :
    (W'.map f).toProjective.polynomialY = MvPolynomial.map f W'.polynomialY

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ (map W' f).toProjective.polynomialY = (MvPolynomial.map f) W'.polynomialY

Tactic:
simp only [polynomialY, map_polynomial, pderiv_map]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {t : RBNode α} :
    t.forM (m := m) f = t.toList.forM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
f : α → m PUnit
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ forM f t = t.toList.forM f

Tactic:
induction t <;> simp [*]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem continuous_lift {hf : ∀ x y, (x ~ᵢ y) → f x = f y} :
    Continuous (lift f hf) ↔ Continuous f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
⊢ Continuous (lift f hf) ↔ Continuous f

Tactic:
simp only [continuous_iff_continuousOn_univ, continuousOn_lift, preimage_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Dual.lean
theorem Matrix.toLin_transpose (M : Matrix ι₁ ι₂ K) : Matrix.toLin B₁.dualBasis B₂.dualBasis Mᵀ =
    Module.Dual.transpose (R := K) (Matrix.toLin B₂ B₁ M)

Proof state:
case a
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis) ((toLin B₁.dualBasis B₂.dualBasis) Mᵀ) =
    (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis) (Module.Dual.transpose ((toLin B₂ B₁) M))

Tactic:
rw [LinearMap.toMatrix_toLin, LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin]

Result:
no goals

Proof state:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ (toLin B₁.dualBasis B₂.dualBasis) Mᵀ = Module.Dual.transpose ((toLin B₂ B₁) M)

Tactic:
apply (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis).injective

Result:
case a
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis) ((toLin B₁.dualBasis B₂.dualBasis) Mᵀ) =
    (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis) (Module.Dual.transpose ((toLin B₂ B₁) M))
-- Mathlib/LinearAlgebra/Prod.lean
theorem coprod_inr (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : (coprod f g).comp (inr R M M₂) = g

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
⊢ f.coprod g ∘ₗ inr R M M₂ = g

Tactic:
ext

Result:
case h
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x✝ : M₂
⊢ (f.coprod g ∘ₗ inr R M M₂) x✝ = g x✝

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x✝ : M₂
⊢ (f.coprod g ∘ₗ inr R M M₂) x✝ = g x✝

Tactic:
simp only [map_zero, coprod_apply, inr_apply, zero_add, comp_apply]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@[simp] lemma edgeSet_coe {G' : G.Subgraph} : G'.coe.edgeSet = Sym2.map (↑) ⁻¹' G'.edgeSet

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.coe.edgeSet = Sym2.map Subtype.val ⁻¹' G'.edgeSet

Tactic:
ext e

Result:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet

Proof state:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet

Tactic:
induction e using Sym2.ind

Result:
case h.h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ y✝ : ↑G'.verts
⊢ s(x✝, y✝) ∈ G'.coe.edgeSet ↔ s(x✝, y✝) ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet

Proof state:
case h.h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ y✝ : ↑G'.verts
⊢ s(x✝, y✝) ∈ G'.coe.edgeSet ↔ s(x✝, y✝) ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem reverseAux_append {u v w x : V}
    (p : G.Walk u v) (q : G.Walk u w) (r : G.Walk w x) :
    (p.reverseAux q).append r = p.reverseAux (q.append r)

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ : V
q : G.Walk u✝ w
⊢ (nil.reverseAux q).append r = nil.reverseAux (q.append r)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (q : G.Walk v✝ w), (p✝.reverseAux q).append r = p✝.reverseAux (q.append r)
q : G.Walk u✝ w
⊢ ((cons h p✝).reverseAux q).append r = (cons h p✝).reverseAux (q.append r)

Tactic:
simp [ih (cons (G.symm h) q)]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk u w
r : G.Walk w x
⊢ (p.reverseAux q).append r = p.reverseAux (q.append r)

Tactic:
induction p with
| nil => rfl
| cons h _ ih => simp [ih (cons (G.symm h) q)]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_sub_right (x y y' : M) : polar Q x (y - y') = polar Q x y - polar Q x y'

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y y' : M
⊢ polar (⇑Q) x (y - y') = polar (⇑Q) x y - polar (⇑Q) x y'

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem induction_on {C : (⨁ i, β i) → Prop} (x : ⨁ i, β i) (H_zero : C 0)
    (H_basic : ∀ (i : ι) (x : β i), C (of β i x))
    (H_plus : ∀ x y, C x → C y → C (x + y)) : C x

Proof state:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C ((of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
ih : C f
⊢ C (DFinsupp.single i b + f)

Tactic:
solve_by_elim

Result:
no goals

Proof state:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C ((of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → C f → C (DFinsupp.single i b + f)

Tactic:
intro i b f h1 h2 ih

Result:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C ((of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
ih : C f
⊢ C (DFinsupp.single i b + f)

Proof state:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C ((of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
⊢ C x

Tactic:
apply DFinsupp.induction x H_zero

Result:
ι : Type v
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : DecidableEq ι
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C ((of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → C f → C (DFinsupp.single i b + f)
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsOpen.div_closure (hs : IsOpen s) (t : Set G) : s / closure t = s / t

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
⊢ s / closure t = s / t

Tactic:
simp_rw [div_eq_mul_inv, inv_closure, hs.mul_closure]

Result:
no goals
-- Mathlib/Algebra/Order/Invertible.lean
theorem invOf_lt_zero [Invertible a] : ⅟ a < 0 ↔ a < 0

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ ⅟a < 0 ↔ a < 0

Tactic:
simp only [← not_le, invOf_nonneg]

Result:
no goals