harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem algEquivOfCompEqX_eq_iff (p q p' q' : R[X])
    (hpq : p.comp q = X) (hqp : q.comp p = X) (hpq' : p'.comp q' = X) (hqp' : q'.comp p' = X) :
    algEquivOfCompEqX p q hpq hqp = algEquivOfCompEqX p' q' hpq' hqp' ↔ p = p' :=
  ⟨fun h ↦ by simpa using congr($h X), fun h ↦ by ext1; simp [h]⟩

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p = p'
a✝ : R[X]
⊢ (p.algEquivOfCompEqX q hpq hqp) a✝ = (p'.algEquivOfCompEqX q' hpq' hqp') a✝

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p = p'
⊢ p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'

Tactic:
ext1

Result:
case h
R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p = p'
a✝ : R[X]
⊢ (p.algEquivOfCompEqX q hpq hqp) a✝ = (p'.algEquivOfCompEqX q' hpq' hqp') a✝

Proof state:
R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'
⊢ p = p'

Tactic:
simpa using congr($h X)

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem inv_app {X Y : Scheme} (f : X ⟶ Y) [IsIso f] (U : X.Opens) :
    (inv f).app U =
      X.presheaf.map (eqToHom (show (f ≫ inv f) ⁻¹ᵁ U = U by rw [IsIso.hom_inv_id]; rfl)).op ≫
        inv (f.app ((inv f) ⁻¹ᵁ U))

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ Hom.app (inv f) U = X.presheaf.map (eqToHom ⋯).op ≫ inv (Hom.app f (inv f ⁻¹ᵁ U))

Tactic:
rw [IsIso.eq_comp_inv, ← Scheme.comp_app, Scheme.congr_app (IsIso.hom_inv_id f),
  Scheme.id_app, Category.id_comp]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ (f ≫ inv f) ⁻¹ᵁ U = U

Tactic:
rw [IsIso.hom_inv_id]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U
-- Mathlib/Computability/TMToPartrec.lean
theorem K'.elim_update_rev {a b c d b'} : update (K'.elim a b c d) rev b' = K'.elim a b' c d

Proof state:
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' = elim a b' c d

Tactic:
funext x

Result:
case h
a b c d b' : List Γ'
x : K'
⊢ update (elim a b c d) rev b' x = elim a b' c d x

Proof state:
case h
a b c d b' : List Γ'
x : K'
⊢ update (elim a b c d) rev b' x = elim a b' c d x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Order/Heyting/Regular.lean
theorem IsRegular.inf (ha : IsRegular a) (hb : IsRegular b) : IsRegular (a ⊓ b)

Proof state:
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a ⊓ b)

Tactic:
rw [IsRegular, compl_compl_inf_distrib, ha.eq, hb.eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Span.lean
theorem iSup_lsingle_range : ⨆ a, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M) = ⊤

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α →₀ M
x✝ : f ∈ ⊤
⊢ f.sum single ∈ ⨆ a, LinearMap.range (lsingle a)

Tactic:
exact sum_mem fun a _ => Submodule.mem_iSup_of_mem a ⟨_, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α →₀ M
x✝ : f ∈ ⊤
⊢ f ∈ ⨆ a, LinearMap.range (lsingle a)

Tactic:
rw [← sum_single f]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α →₀ M
x✝ : f ∈ ⊤
⊢ f.sum single ∈ ⨆ a, LinearMap.range (lsingle a)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⨆ a, LinearMap.range (lsingle a) = ⊤

Tactic:
refine eq_top_iff.2 <| SetLike.le_def.2 fun f _ => ?_

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α →₀ M
x✝ : f ∈ ⊤
⊢ f ∈ ⨆ a, LinearMap.range (lsingle a)
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.ne_zero [Nontrivial R] {p : Fin 2 → R} (h : IsCoprime (p 0) (p 1)) : p ≠ 0

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : IsCoprime (0 0) (0 1)
⊢ False

Tactic:
exact not_isCoprime_zero_zero h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
p : Fin 2 → R
h : IsCoprime (p 0) (p 1)
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : IsCoprime (0 0) (0 1)
⊢ False
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensorHom_id {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
    f ⊗ 𝟙 Y = f ▷ Y

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ f ⊗ 𝟙 Y = f ▷ Y

Tactic:
simp [tensorHom_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem mkGate_le_size (aig : AIG α) (input : GateInput aig) :
    aig.decls.size ≤ (aig.mkGate input).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
⊢ aig.decls.size ≤ (aig.mkGate input).aig.decls.size

Tactic:
simp_arith [mkGate]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem comap_map_of_surjective (hf : Function.Surjective f) (I : Ideal R) :
    comap f (map f I) = I ⊔ comap f ⊥ :=
  le_antisymm
    (fun r h =>
      let ⟨s, hsi, hfsr⟩ := mem_image_of_mem_map_of_surjective f hf h
      Submodule.mem_sup.2
        ⟨s, hsi, r - s, (Submodule.mem_bot S).2 <| by rw [map_sub, hfsr, sub_self],
          add_sub_cancel s r⟩)
    (sup_le (map_le_iff_le_comap.1 le_rfl) (comap_mono bot_le))

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
r : R
h : f r ∈ map f I
s : R
hsi : s ∈ ↑I
hfsr : f s = f r
⊢ f (r - s) = 0

Tactic:
rw [map_sub, hfsr, sub_self]

Result:
no goals
-- Mathlib/Algebra/Module/CharacterModule.lean
lemma dual_comp {C : Type*} [AddCommGroup C] [Module R C] (f : A →ₗ[R] B) (g : B →ₗ[R] C) :
    dual (g.comp f) = (dual f).comp (dual g)

Proof state:
case h.h
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
B : Type uB
inst✝⁴ : AddCommGroup B
inst✝³ : Module R A
inst✝² : Module R B
C : Type u_2
inst✝¹ : AddCommGroup C
inst✝ : Module R C
f : A →ₗ[R] B
g : B →ₗ[R] C
x✝¹ : CharacterModule C
x✝ : A
⊢ ((dual (g ∘ₗ f)) x✝¹) x✝ = ((dual f ∘ₗ dual g) x✝¹) x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
B : Type uB
inst✝⁴ : AddCommGroup B
inst✝³ : Module R A
inst✝² : Module R B
C : Type u_2
inst✝¹ : AddCommGroup C
inst✝ : Module R C
f : A →ₗ[R] B
g : B →ₗ[R] C
⊢ dual (g ∘ₗ f) = dual f ∘ₗ dual g

Tactic:
ext

Result:
case h.h
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
B : Type uB
inst✝⁴ : AddCommGroup B
inst✝³ : Module R A
inst✝² : Module R B
C : Type u_2
inst✝¹ : AddCommGroup C
inst✝ : Module R C
f : A →ₗ[R] B
g : B →ₗ[R] C
x✝¹ : CharacterModule C
x✝ : A
⊢ ((dual (g ∘ₗ f)) x✝¹) x✝ = ((dual f ∘ₗ dual g) x✝¹) x✝
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem eq_of_le_of_finrank_le {S₁ S₂ : Submodule K V} [FiniteDimensional K S₂] (hle : S₁ ≤ S₂)
    (hd : finrank K S₂ ≤ finrank K S₁) : S₁ = S₂

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
S₁ S₂ : Submodule K V
inst✝ : FiniteDimensional K ↥S₂
hle : S₁ ≤ S₂
hd : finrank K ↥S₂ ≤ finrank K ↥(comap S₂.subtype S₁)
⊢ S₁ = S₂

Tactic:
exact le_antisymm hle (Submodule.comap_subtype_eq_top.1
  (eq_top_of_finrank_eq (le_antisymm (comap (Submodule.subtype S₂) S₁).finrank_le hd)))

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
S₁ S₂ : Submodule K V
inst✝ : FiniteDimensional K ↥S₂
hle : S₁ ≤ S₂
hd : finrank K ↥S₂ ≤ finrank K ↥S₁
⊢ S₁ = S₂

Tactic:
rw [← LinearEquiv.finrank_eq (Submodule.comapSubtypeEquivOfLe hle)] at hd

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
S₁ S₂ : Submodule K V
inst✝ : FiniteDimensional K ↥S₂
hle : S₁ ≤ S₂
hd : finrank K ↥S₂ ≤ finrank K ↥(comap S₂.subtype S₁)
⊢ S₁ = S₂
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem OrientedOrd.instLexOrd [Ord α] [Ord β]
    [OrientedOrd α] [OrientedOrd β] : @OrientedOrd (α × β) lexOrd

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Ord α
inst✝² : Ord β
inst✝¹ : OrientedOrd α
inst✝ : OrientedOrd β
⊢ OrientedCmp (compareLex (compareOn fun x => x.fst) (compareOn fun x => x.snd))

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Ord α
inst✝² : Ord β
inst✝¹ : OrientedOrd α
inst✝ : OrientedOrd β
⊢ OrientedOrd (α × β)

Tactic:
rw [OrientedOrd, lexOrd_def]

Result:
α : Type u_1
β : Type u_2
inst✝³ : Ord α
inst✝² : Ord β
inst✝¹ : OrientedOrd α
inst✝ : OrientedOrd β
⊢ OrientedCmp (compareLex (compareOn fun x => x.fst) (compareOn fun x => x.snd))
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem IsIntegral.of_pow [Algebra R B] {x : B} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R <| x ^ n) :
    IsIntegral R x :=
  have ⟨p, hmonic, heval⟩ := hx
  ⟨expand R n p, hmonic.expand hn, by rwa [← aeval_def, expand_aeval]⟩

Proof state:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R B) (x ^ n) p = 0
⊢ eval₂ (algebraMap R B) x ((expand R n) p) = 0

Tactic:
rwa [← aeval_def, expand_aeval]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_self_ne_one : ∀ n, n + n ≠ 1
  | n+1, h => by rw [Nat.succ_add, Nat.succ.injEq] at h; contradiction

Proof state:
n : Nat
h : n + 1 + (n + 1) = 1
⊢ False

Tactic:
rw [Nat.succ_add, Nat.succ.injEq] at h

Result:
n : Nat
h : n + (n + 1) = 0
⊢ False

Proof state:
n : Nat
h : n + (n + 1) = 0
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem sSup_atoms_eq_top : sSup { a : α | IsAtom a } = ⊤

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
⊢ sSup {a | IsAtom a} = ⊤

Tactic:
refine Eq.trans (congr rfl (Set.ext fun x => ?_)) (sSup_atoms_le_eq ⊤)

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
x : α
⊢ x ∈ {a | IsAtom a} ↔ x ∈ {a | IsAtom a ∧ a ≤ ⊤}

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
x : α
⊢ x ∈ {a | IsAtom a} ↔ x ∈ {a | IsAtom a ∧ a ≤ ⊤}

Tactic:
exact (and_iff_left le_top).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0

Proof state:
α : Type u_1
l : List α
⊢ l.isEmpty = true ↔ l.length = 0

Tactic:
rw [isEmpty_iff, length_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem aeval_eq_smeval {R : Type*} [CommSemiring R] {S : Type*} [Semiring S] [Algebra R S]
    (x : S) (p : R[X]) : aeval x p = p.smeval x

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ (aeval x) p = p.smeval x

Tactic:
rw [aeval_def, eval₂_def, Algebra.algebraMap_eq_smul_one', smeval_def]

Result:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ (p.sum fun e a => (fun r => r • 1) a * x ^ e) = p.sum (smul_pow x)

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ (p.sum fun e a => a • x ^ e) = p.sum (smul_pow x)

Tactic:
exact rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ (p.sum fun e a => (fun r => r • 1) a * x ^ e) = p.sum (smul_pow x)

Tactic:
simp only [Algebra.smul_mul_assoc, one_mul]

Result:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ (p.sum fun e a => a • x ^ e) = p.sum (smul_pow x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
    (zipWith f as bs).toList = List.zipWith f as.toList bs.toList

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
as : Array α
bs : Array β
⊢ (zipWith f as bs).toList = List.zipWith f as.toList bs.toList

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
bs : Array β
toList✝ : List α
⊢ (zipWith f { toList := toList✝ } bs).toList = List.zipWith f { toList := toList✝ }.toList bs.toList

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
bs : Array β
toList✝ : List α
⊢ (zipWith f { toList := toList✝ } bs).toList = List.zipWith f { toList := toList✝ }.toList bs.toList

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝¹ : List α
toList✝ : List β
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ }).toList =
    List.zipWith f { toList := toList✝¹ }.toList { toList := toList✝ }.toList

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝¹ : List α
toList✝ : List β
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ }).toList =
    List.zipWith f { toList := toList✝¹ }.toList { toList := toList✝ }.toList

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.extendScalars (hinj : Function.Injective (algebraMap R S)) {x : A}
    (A_alg : IsAlgebraic R x) : IsAlgebraic S x :=
  let ⟨p, hp₁, hp₂⟩ := A_alg
  ⟨p.map (algebraMap _ _), by
    rwa [Ne, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot], by simpa⟩

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ⇑(algebraMap R S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : (aeval x) p = 0
⊢ map (algebraMap R S) p ≠ 0

Tactic:
rwa [Ne, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot]

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ⇑(algebraMap R S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : (aeval x) p = 0
⊢ (aeval x) (map (algebraMap R S) p) = 0

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem to_ring_inverse (e : M ≃L[R] M₂) (f : M →L[R] M₂) :
    inverse f = Ring.inverse ((e.symm : M₂ →L[R] M).comp f) ∘L e.symm

Proof state:
case pos
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : f.IsInvertible
⊢ f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

Tactic:
obtain ⟨e', he'⟩ := h₁

Result:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

Proof state:
case h.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
x✝ : M
⊢ ↑(((ContinuousLinearEquiv.unitsEquiv R M) F).trans e) x✝ = f x✝

Tactic:
dsimp

Result:
case h.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
x✝ : M
⊢ e (↑F x✝) = f x✝

Proof state:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ (↑e').inverse = (Ring.inverse ((↑e.symm).comp ↑e')).comp ↑e.symm

Tactic:
change _ = Ring.inverse (e'.trans e.symm : M →L[R] M) ∘L (e.symm : M₂ →L[R] M)

Result:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ (↑e').inverse = (Ring.inverse ↑(e'.trans e.symm)).comp ↑e.symm

Proof state:
case h.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
x✝ : M
⊢ e (↑F x✝) = f x✝

Tactic:
rw [hF]

Result:
case h.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = (↑e.symm).comp f
x✝ : M
⊢ e (((↑e.symm).comp f) x✝) = f x✝
-- Mathlib/Data/ZMod/Basic.lean
lemma ZModModule.two_le_char [NeZero n] [Nontrivial G] : 2 ≤ n

Proof state:
n : ℕ
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module (ZMod n) G
inst✝¹ : NeZero n
inst✝ : Nontrivial G
this✝ : n ≠ 0
this : n ≠ 1
⊢ 2 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module (ZMod n) G
inst✝¹ : NeZero n
inst✝ : Nontrivial G
this : n ≠ 0
⊢ 2 ≤ n

Tactic:
have := char_ne_one n G

Result:
n : ℕ
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module (ZMod n) G
inst✝¹ : NeZero n
inst✝ : Nontrivial G
this✝ : n ≠ 0
this : n ≠ 1
⊢ 2 ≤ n

Proof state:
n : ℕ
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module (ZMod n) G
inst✝¹ : NeZero n
inst✝ : Nontrivial G
⊢ 2 ≤ n

Tactic:
have := NeZero.ne n

Result:
n : ℕ
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module (ZMod n) G
inst✝¹ : NeZero n
inst✝ : Nontrivial G
this : n ≠ 0
⊢ 2 ≤ n
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem invOfUnit_eq' (φ : MvPowerSeries σ k) (u : Units k) (h : constantCoeff σ k φ = u) :
    invOfUnit φ u = φ⁻¹

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff σ k) φ = ↑u
⊢ u = Units.mk0 ((constantCoeff σ k) φ) ⋯

Tactic:
rw [Units.ext_iff]

Result:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff σ k) φ = ↑u
⊢ ↑u = ↑(Units.mk0 ((constantCoeff σ k) φ) ⋯)

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff σ k) φ = ↑u
⊢ ↑u = ↑(Units.mk0 ((constantCoeff σ k) φ) ⋯)

Tactic:
exact h.symm

Result:
no goals

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff σ k) φ = ↑u
⊢ φ.invOfUnit u = φ.invOfUnit (Units.mk0 ((constantCoeff σ k) φ) ⋯)

Tactic:
apply congrArg (invOfUnit φ)

Result:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff σ k) φ = ↑u
⊢ u = Units.mk0 ((constantCoeff σ k) φ) ⋯

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff σ k) φ = ↑u
⊢ φ.invOfUnit u = φ⁻¹

Tactic:
rw [← invOfUnit_eq φ (h.symm ▸ u.ne_zero)]

Result:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff σ k) φ = ↑u
⊢ φ.invOfUnit u = φ.invOfUnit (Units.mk0 ((constantCoeff σ k) φ) ⋯)
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem rightAngleRotationAux₁_rightAngleRotationAux₁ (x : E) :
    o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
this : inner (o.rightAngleRotationAux₁ y) (o.rightAngleRotationAux₁ x) = inner y x
⊢ inner y (o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)) = inner y (-x)

Tactic:
rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this,
  inner_neg_right]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x

Tactic:
apply ext_inner_left ℝ

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ∀ (v : E), inner v (o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)) = inner v (-x)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner y (o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)) = inner y (-x)

Tactic:
have : ⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫ = ⟪y, x⟫ :=
  LinearIsometry.inner_map_map o.rightAngleRotationAux₂ y x

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
this : inner (o.rightAngleRotationAux₁ y) (o.rightAngleRotationAux₁ x) = inner y x
⊢ inner y (o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)) = inner y (-x)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ∀ (v : E), inner v (o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)) = inner v (-x)

Tactic:
intro y

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner y (o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)) = inner y (-x)
-- Mathlib/Data/List/Duplicate.lean
theorem Duplicate.ne_singleton (h : x ∈+ l) (y : α) : l ≠ [y]

Proof state:
α : Type u_1
l : List α
x : α
h : x ∈+ l
y : α
⊢ l ≠ [y]

Tactic:
induction' h with l' h z l' h _

Result:
case cons_mem
α : Type u_1
l : List α
x y : α
l' : List α
h : x ∈ l'
⊢ x :: l' ≠ [y]

case cons_duplicate
α : Type u_1
l : List α
x y z : α
l' : List α
h : x ∈+ l'
a_ih✝ : l' ≠ [y]
⊢ z :: l' ≠ [y]

Proof state:
case cons_duplicate
α : Type u_1
l : List α
x y z : α
l' : List α
h : x ∈+ l'
a_ih✝ : l' ≠ [y]
⊢ z :: l' ≠ [y]

Tactic:
simp [ne_nil_of_mem h.mem]

Result:
no goals

Proof state:
case cons_mem
α : Type u_1
l : List α
x y : α
l' : List α
h : x ∈ l'
⊢ x :: l' ≠ [y]

Tactic:
simp [ne_nil_of_mem h]

Result:
no goals