harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem toLin_toMatrix [Finite ι] [Fintype ι'] [DecidableEq ι'] (v : Basis ι' R M) :
    Matrix.toLin v e (e.toMatrix v) = LinearMap.id :=
  v.ext fun i => by cases nonempty_fintype ι; rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
val✝ : Fintype ι
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)

Proof state:
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
val✝ : Fintype ι
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)

Tactic:
rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insertIfNew [LawfulBEq α] (h : m.WF) {k a : α} [Inhabited (β a)] {v : β k} :
    (m.insertIfNew k v).get! a =
      if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v else m.get! a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.get! a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get! a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get! a

Tactic:
simp_to_raw using Raw₀.get!_insertIfNew ⟨m, _⟩

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map_eq_mapAccumr {f : α → β} :
    map f xs = (mapAccumr (fun x (_ : Unit) ↦ ((), f x)) xs ()).snd

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
⊢ map f xs = (mapAccumr (fun x x_1 => ((), f x)) xs ()).2

Tactic:
induction xs using Vector.revInductionOn <;> simp_all

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_lt_iff_lt_rpow_of_base_lt_one (hx : 0 < x) : logb b x < y ↔ b ^ y < x

Proof state:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x < y ↔ b ^ y < x

Tactic:
rw [← rpow_lt_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hx]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma iIndep_zero_right : iIndep m κ 0

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
⊢ iIndep m κ 0

Tactic:
simp [iIndep]

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/MonoidAlgebra.lean
theorem comul_C_mul_T (a : A) (n : ℤ) :
    Coalgebra.comul (R := R) (C a * T n) =
      TensorProduct.map (lsingle n) (lsingle n) (Coalgebra.comul (R := R) a)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
n : ℤ
⊢ CoalgebraStruct.comul (C a * T n) = (TensorProduct.map (lsingle n) (lsingle n)) (CoalgebraStruct.comul a)

Tactic:
simp [← single_eq_C_mul_T]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Seminorm.lean
theorem smul_sup (r : R) (p q : AddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
  have Real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
    simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
  ext fun _ => Real.smul_max _ _

Proof state:
R : Type u_1
E : Type u_3
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : AddGroupSeminorm E
x y : ℝ
⊢ r • (x ⊔ y) = r • x ⊔ r • y

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
  mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma levyProkhorovEDist_lt_top (μ ν : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    levyProkhorovEDist μ ν < ∞ :=
  (levyProkhorovEDist_le_max_measure_univ μ ν).trans_lt <| by simp [measure_lt_top]

Proof state:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ univ ⊔ ν univ < ⊤

Tactic:
simp [measure_lt_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
    enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id)

Proof state:
α : Type u_1
n : Nat
x : α
xs : List α
⊢ enumFrom n (x :: xs) = (n, x) :: map (Prod.map (fun x => x + 1) id) (enumFrom n xs)

Tactic:
rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem mem_or_not_mem (φ : L.Sentence) : φ ∈ L.completeTheory M ∨ φ.not ∈ L.completeTheory M

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M

Tactic:
simp_rw [completeTheory, Set.mem_setOf_eq, Sentence.Realize, Formula.realize_not, or_not]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem IsHermitian.transpose {A : Matrix n n α} (h : A.IsHermitian) : Aᵀ.IsHermitian

Proof state:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ (Aᵀ.map star)ᵀ = Aᵀ

Tactic:
exact congr_arg Matrix.transpose h

Result:
no goals

Proof state:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ Aᵀ.IsHermitian

Tactic:
rw [IsHermitian, conjTranspose, transpose_map]

Result:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ (Aᵀ.map star)ᵀ = Aᵀ
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_nonsingular (hf : Function.Injective f) :
    (W'.map f).toAffine.Nonsingular (f x) (f y) ↔ W'.Nonsingular x y

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y : R
hf : Function.Injective ⇑f
⊢ (map W' f).toAffine.Nonsingular (f x) (f y) ↔ W'.Nonsingular x y

Tactic:
simp only [Nonsingular, evalEval, map_equation _ _ hf, map_polynomialX, map_polynomialY,
  map_mapRingHom_evalEval, map_ne_zero_iff f hf]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem full_mono {D E : Set C} (h : D ≤ E) : full D ≤ full E

Proof state:
C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ≤ E
⊢ ∀ {c d : C}, (full D).arrows c d ⊆ (full E).arrows c d

Tactic:
rintro c d f

Result:
C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ≤ E
c d : C
f : c ⟶ d
⊢ f ∈ (full D).arrows c d → f ∈ (full E).arrows c d

Proof state:
C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ≤ E
c d : C
f : c ⟶ d
⊢ f ∈ (full D).arrows c d → f ∈ (full E).arrows c d

Tactic:
simp only [mem_full_iff]

Result:
C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ≤ E
c d : C
f : c ⟶ d
⊢ c ∈ D ∧ d ∈ D → c ∈ E ∧ d ∈ E

Proof state:
C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ≤ E
⊢ full D ≤ full E

Tactic:
rw [le_iff]

Result:
C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ≤ E
⊢ ∀ {c d : C}, (full D).arrows c d ⊆ (full E).arrows c d

Proof state:
C : Type u
inst✝ : Groupoid C
D E : Set C
h : D ≤ E
c d : C
f : c ⟶ d
⊢ c ∈ D ∧ d ∈ D → c ∈ E ∧ d ∈ E

Tactic:
exact fun ⟨hc, hd⟩ => ⟨h hc, h hd⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem dite_cond_eq_true' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c → α} {b : ¬ c → α} {r : α} (h₁ : c = True) (h₂ : a (of_eq_true h₁) = r) : (dite c a b) = r

Proof state:
α : Sort u
c : Prop
x✝ : Decidable c
a : c → α
b : ¬c → α
r : α
h₁ : c = True
h₂ : a ⋯ = r
⊢ dite c a b = r

Tactic:
simp [h₁, h₂]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
theorem ne_zero_iff {p : RingSeminorm R} : p ≠ 0 ↔ ∃ x, p x ≠ 0

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
p : RingSeminorm R
⊢ p ≠ 0 ↔ ∃ x, p x ≠ 0

Tactic:
simp [eq_zero_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem IntervalIntegrable.congr {g : ℝ → E} (hf : IntervalIntegrable f μ a b)
    (h : f =ᵐ[μ.restrict (Ι a b)] g) :
    IntervalIntegrable g μ a b

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
g : ℝ → E
hf : IntervalIntegrable f μ a b
h : f =ᶠ[ae (μ.restrict (Ι a b))] g
⊢ IntervalIntegrable g μ a b

Tactic:
rwa [intervalIntegrable_iff, ← integrableOn_congr_fun_ae h, ← intervalIntegrable_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem HasFiniteIntegral.norm {f : α → β} (hfi : HasFiniteIntegral f μ) :
    HasFiniteIntegral (fun a => ‖f a‖) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (fun a => ‖f a‖) μ

Tactic:
simpa [hasFiniteIntegral_iff_enorm] using hfi

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_sUnion {S : Set (Set α)} (hS : S.Finite) (a : α) :
    𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : S.Finite
a : α
⊢ 𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a

Tactic:
rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]

Result:
no goals
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[simp]
lemma ofPoint_SpecTensorTo (T : Triplet f g) (p : Spec T.tensor) :
    ofPoint (T.SpecTensorTo.base p) = T

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ ofPoint ((ConcreteCategory.hom T.SpecTensorTo.base) p) = T

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
theorem whiskerLeft_naturality_comp (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) :
    f ◁ θ.naturality (g ≫ h) ≫ f ◁ θ.app a ◁ H.mapComp g h =
      f ◁ G.mapComp g h ▷ θ.app c ≫
        f ◁ (α_ _ _ _).hom ≫
          f ◁ G.map g ◁ θ.naturality h ≫
            f ◁ (α_ _ _ _).inv ≫ f ◁ θ.naturality g ▷ H.map h ≫ f ◁ (α_ _ _ _).hom

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
G H : OplaxFunctor B C
θ : OplaxNatTrans G H
a b c : B
a' : C
f : a' ⟶ G.obj a
g : a ⟶ b
h : b ⟶ c
⊢ f ◁ θ.naturality (g ≫ h) ≫ f ◁ θ.app a ◁ H.mapComp g h =
    f ◁ G.mapComp g h ▷ θ.app c ≫
      f ◁ (α_ (G.map g) (G.map h) (θ.app c)).hom ≫
        f ◁ G.map g ◁ θ.naturality h ≫
          f ◁ (α_ (G.map g) (θ.app b) (H.map h)).inv ≫
            f ◁ θ.naturality g ▷ H.map h ≫ f ◁ (α_ (θ.app a) (H.map g) (H.map h)).hom

Tactic:
simp_rw [← Bicategory.whiskerLeft_comp, naturality_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/OfFn.lean
theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFn f = [] ↔ n = 0

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
⊢ ofFn f = [] ↔ n = 0

Tactic:
cases n <;> simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero, reduceCtorEq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_multiset_prod_le : t.prod.natDegree ≤ (t.map natDegree).sum :=
  Quotient.inductionOn t (by simpa using natDegree_list_prod_le)

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), (prod ⟦a⟧).natDegree ≤ (Multiset.map natDegree ⟦a⟧).sum

Tactic:
simpa using natDegree_list_prod_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w))

Proof state:
w : Nat
x : BitVec (w + 1)
⊢ x = cons x.msb (setWidth w x)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Restrict.lean
theorem AffineMap.restrict.injective {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Injective φ)
    {E : AffineSubspace k P₁} {F : AffineSubspace k P₂} [Nonempty E] [Nonempty F]
    (hEF : E.map φ ≤ F) : Function.Injective (AffineMap.restrict φ hEF)

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
h : (φ.restrict hEF) x = (φ.restrict hEF) y
⊢ x = y

Tactic:
simp only [Subtype.ext_iff, Subtype.coe_mk, AffineMap.restrict.coe_apply] at h ⊢

Result:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
h : φ ↑x = φ ↑y
⊢ ↑x = ↑y

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ Function.Injective ⇑(φ.restrict hEF)

Tactic:
intro x y h

Result:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
h : (φ.restrict hEF) x = (φ.restrict hEF) y
⊢ x = y

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
h : φ ↑x = φ ↑y
⊢ ↑x = ↑y

Tactic:
exact hφ h

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem hnot_bot : ￢(⊥ : α) = ⊤ :=
  eq_of_forall_ge_iff fun a => by rw [hnot_le_iff_codisjoint_left, codisjoint_bot, top_le_iff]

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢⊥ ≤ a ↔ ⊤ ≤ a

Tactic:
rw [hnot_le_iff_codisjoint_left, codisjoint_bot, top_le_iff]

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma not_exists_sq' : m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n

Proof state:
m n : ℕ
⊢ m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n

Tactic:
simpa only [Nat.pow_two] using not_exists_sq

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
lemma Set.Finite.cofinite_inf_principal_compl {s : Set α} (hs : s.Finite) :
    cofinite ⊓ 𝓟 sᶜ = cofinite

Proof state:
α : Type u_2
s : Set α
hs : s.Finite
⊢ cofinite ⊓ 𝓟 sᶜ = cofinite

Tactic:
simpa using hs.compl_mem_cofinite

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma r1_eq : r1 z = 1 / ((z.re / z.im) ^ 2 + 1)

Proof state:
z : ℍ
⊢ z.im ^ 2 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
z : ℍ
⊢ r1 z = 1 / ((z.re / z.im) ^ 2 + 1)

Tactic:
rw [div_pow, div_add_one (by positivity), one_div_div, r1]

Result:
no goals
-- Mathlib/Order/Heyting/Hom.lean
theorem cancel_left (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => HeytingHom.ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingAlgebra γ
f₁ f₂ : HeytingHom α β
g : HeytingHom β γ
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Ici_mul_Ici_subset' [LocallyFiniteOrderTop α] (a b : α) : Ici a * Ici b ⊆ Ici (a * b) :=
  Finset.coe_subset.mp <| by simpa using Set.Ici_mul_Ici_subset' _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : Preorder α
inst✝³ : DecidableEq α
inst✝² : MulLeftMono α
inst✝¹ : MulRightMono α
inst✝ : LocallyFiniteOrderTop α
a b : α
⊢ ↑(Ici a * Ici b) ⊆ ↑(Ici (a * b))

Tactic:
simpa using Set.Ici_mul_Ici_subset' _ _

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma μ_snd (X Y : C) : LaxMonoidal.μ F X Y ≫ F.map (snd X Y) = snd (F.obj X) (F.obj Y) :=
  (cancel_epi (μIso _ _ _).inv).1 (by simp)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).inv ≫ LaxMonoidal.μ F X Y ≫ F.map (snd X Y) = (μIso F X Y).inv ≫ snd (F.obj X) (F.obj Y)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc]
lemma inlX_d (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) :
    inlX φ j i hij ≫ d φ i j = -F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j

Proof state:
case h₂
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ (inlX φ j i hij ≫ d φ i j) ≫ sndX φ j = (-F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j) ≫ sndX φ j

Tactic:
simp [d_sndX φ _ _ hij]

Result:
no goals

Proof state:
case h₁
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ (inlX φ j i hij ≫ d φ i j) ≫ fstX φ j k hjk = (-F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j) ≫ fstX φ j k hjk

Tactic:
simp [d_fstX φ  _ _ _ hij hjk]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ inlX φ j i hij ≫ d φ i j = -F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j

Tactic:
apply ext_to_X φ j k hjk

Result:
case h₁
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ (inlX φ j i hij ≫ d φ i j) ≫ fstX φ j k hjk = (-F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j) ≫ fstX φ j k hjk

case h₂
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ (inlX φ j i hij ≫ d φ i j) ≫ sndX φ j = (-F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j) ≫ sndX φ j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem isNone_unattach {p : α → Prop} {o : Option { x // p x }} :
    o.unattach.isNone = o.isNone

Proof state:
α : Type u_1
p : α → Prop
o : Option { x // p x }
⊢ o.unattach.isNone = o.isNone

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem symmL_model_space (b b' : F) :
    (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b).symmL 𝕜 b' = (1 : F →L[𝕜] F)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
b b' : F
⊢ b' ∈ (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b).baseSet

Tactic:
apply mem_univ

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
b b' : F
⊢ Trivialization.symmL 𝕜 (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b) b' = 1

Tactic:
rw [TangentBundle.trivializationAt_symmL, coordChange_model_space]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
b b' : F
⊢ b' ∈ (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b).baseSet
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem isRight_swap (x : α ⊕ β) : x.swap.isRight = x.isLeft

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ x.swap.isRight = x.isLeft

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem le_cof [IsRefl α r] (c : Cardinal) :
    c ≤ cof r ↔ ∀ {S : Set α}, (∀ a, ∃ b ∈ S, r a b) → c ≤ #S

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal.{u}
⊢ c ≤ cof r ↔ ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S

Tactic:
rw [cof, le_csInf_iff'' (cof_nonempty r)]

Result:
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal.{u}
⊢ (∀ b ∈ {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}, c ≤ b) ↔ ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S

Proof state:
case mpr.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal.{u}
H : ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S
S : Set α
h : ∀ (a : α), ∃ b ∈ S, r a b
⊢ c ≤ #↑S

Tactic:
exact H h

Result:
no goals

Proof state:
case mpr
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal.{u}
⊢ (∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S) → ∀ b ∈ {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}, c ≤ b

Tactic:
rintro H d ⟨S, h, rfl⟩

Result:
case mpr.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal.{u}
H : ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S
S : Set α
h : ∀ (a : α), ∃ b ∈ S, r a b
⊢ c ≤ #↑S

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal.{u}
⊢ (∀ b ∈ {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}, c ≤ b) ↔ ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S

Tactic:
use fun H S h => H _ ⟨S, h, rfl⟩

Result:
case mpr
α : Type u
r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal.{u}
⊢ (∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S) → ∀ b ∈ {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}, c ≤ b
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Path.cast_cons {u v w u' w' : U} (p : Path u v) (e : v ⟶ w) (hu : u = u') (hw : w = w') :
    (p.cons e).cast hu hw = (p.cast hu rfl).cons (e.cast rfl hw)

Proof state:
U : Type u_1
inst✝ : Quiver U
v u' w' : U
p : Path u' v
e : v ⟶ w'
⊢ cast ⋯ ⋯ (p.cons e) = (cast ⋯ ⋯ p).cons (Hom.cast ⋯ ⋯ e)

Tactic:
rfl

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u v w u' w' : U
p : Path u v
e : v ⟶ w
hu : u = u'
hw : w = w'
⊢ cast hu hw (p.cons e) = (cast hu ⋯ p).cons (Hom.cast ⋯ hw e)

Tactic:
subst_vars

Result:
U : Type u_1
inst✝ : Quiver U
v u' w' : U
p : Path u' v
e : v ⟶ w'
⊢ cast ⋯ ⋯ (p.cons e) = (cast ⋯ ⋯ p).cons (Hom.cast ⋯ ⋯ e)
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem comp_appLE {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U V e) :
    (f ≫ g).appLE U V e = g.app U ≫ f.appLE _ V e

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : X.Opens
e : V ≤ (f ≫ g) ⁻¹ᵁ U
⊢ Hom.appLE (f ≫ g) U V e = Hom.app g U ≫ Hom.appLE f (g ⁻¹ᵁ U) V e

Tactic:
rw [g.app_eq_appLE, appLE_comp_appLE]

Result:
no goals